X:Type{j}, ds:fpf(Id; x.Type{i}), da:fpf(Knd; k.Type{i}), x:ecl(ds; da),
base:(k:Knd(decl-state(ds)ma-valtype(da; k))X),
seq,and,or:(ecl(ds; da)ecl(ds; da)XXX), repeat:(ecl(ds; da)XX),
act,throw:(ecl(ds; da)XX), catch:(ecl(ds; da)( List)XX).
ecl_ind(x;
ecl_ind(k,test.base(k,test);
ecl_ind(a,b,rec1,rec2.seq(a,b,rec1,rec2);
ecl_ind(a,b,rec1,rec2.and(a,b,rec1,rec2);
ecl_ind(a,b,rec1,rec2.or(a,b,rec1,rec2);
ecl_ind(a,rec1.repeat(a,rec1);
ecl_ind(a,n,rec1.act(a,n,rec1);
ecl_ind(a,n,rec1.throw(a,n,rec1);
ecl_ind(a,l,rec1.catch(a,l,rec1))
 X 

latex

Definitions	x. t(x), t.2, t.1, Y, x(s1,s2,s3), x(s1,s2,s3,s4), x(s1,s2), ecl ind, t  T, ecl(ds; da), x:A. B(x), x(s)
Lemmas	Id wf, fpf wf, ecl wf, Knd wf, nat wf, bool wf, ma-valtype wf, decl-state wf